(set-option :proof true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const i0 Int)
(declare-const i3 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i9 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i12 Int)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (exists ((q0 Bool) (q1 Bool)) (not (and q1 v2 v13 v12 q1 q1 v3 q1))))
(assert (exists ((q2 Bool) (q3 Bool)) (not (= v8 q2 q3 q3 v13 (=> v3 v10) q2 q3 q2 q2))))
(declare-const v17 Bool)
(assert (not (exists ((q4 Int) (q5 Int)) v4)))
(assert (exists ((q4 Int) ) (forall ((q5 Int) ) (not (> (+ i3 i11 51 60) 13)))))
(assert (not (exists ((q6 Bool)) (not (=> v17 (= i12 i6))))))
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const v21 Bool)
(declare-const i15 Int)
(declare-const i16 Int)
(declare-const i17 Int)
(declare-const v22 Bool)
(assert (exists ((q7 Bool) (q8 Int) (q9 Bool)) v6))
(declare-const v23 Bool)
(declare-const i18 Int)
(assert (forall ((q10 Int) (q11 Bool) (q12 Int)) (not (<= q12 q10))))
(declare-const v24 Bool)
(assert (or v17))
(assert (or v6))
(assert (or (= v2 (not (= 228 439)) v0 v4 v12) v14 v0 v24 v14 v14 (= v2 (not (= 228 439)) v0 v4 v12)))
(assert (or v4))
(assert (or v6 v21 v18 (< 723 13) (= v2 (not (= 228 439)) v0 v4 v12)))
(assert (or v18 v0 v14))
(assert (or v17 v10 v14 v17))
(assert (or (<= i5 i9) v10))
(assert (or v0))
(assert (or v10 v19 v17 v6 v12 v12 v24))
(assert (or v10 v4))
(assert (or v6 (<= i5 i9) (<= i5 i9)))
(assert (or v21))
(assert (or v10))
(assert (or v12 v6 v21 v17))
(assert (or v0 v10 v14))
(assert (or v24))
(assert (or v18 v14))
(assert (or v0 (< 723 13)))
(assert (or v18 (< 723 13)))
(assert (or v6 v14 v0 v18))
(assert (or v14 v17 v21))
(assert (or v21))
(assert (or v18 (< 723 13) v19 v0 v0 v21 v10 v24 (<= i5 i9)))
(assert (or v10 v0 v19 v14 v17 v17 (<= i5 i9) v18))
(assert (or v18 v18 (< 723 13) v10 (< 723 13) (= v2 (not (= 228 439)) v0 v4 v12) v4))
(assert (or (< 723 13) (<= i5 i9)))
(assert (or v18))
(assert (or v24 (<= i5 i9) v14 v6))
(assert (or v17 v14 v21 v17))
(check-sat-using qe_rec)
